;; Suppose we wanted to check assumptions about arguments to
;; our function. What kind of form could we write to express
;; this?

;; (define-with-contract account-withdraw
;;   (requires (< amount account-balance))
;;   (ensures (>= account-balance 0))
;;   (lambda (amount account-balance)
;;     ...))

;; Or abstractly:

;; (define-with-contract func
;;   (requires req-pred* ...)
;;   (ensures ensure-pred* ...)
;;   lambda-expr)


;; We make a proper module, so that the bindings in this
;; module can be imported in other modules. It also allows
;; for things like (import (prefix (contract) contract:)),
;; which prefixes all things from this module.
(library (contract)
  (export require
          ensure
          define-with-contract
          define*-with-contract
          lambda-with-contract
          lambda*-with-contract
          λ-with-contract
          λ*-with-contract
          <?>)
  (import
   (except (rnrs base) let-values)
   (only (guile)
         lambda* λ
         syntax-error)
   ;; standard library stuff
   (ice-9 exceptions)
   ;; SRFIs
   (srfi srfi-9 gnu)
   (srfi srfi-1)
   ;; CK style macro stuff
   (ck-base)
   (ck-extra)
   ;; custom exceptions
   (exceptions))


  ;; Define `require` and `ensure`, so that they are
  ;; available as identifiers. This will cause syntax-rules
  ;; to be aware of them as identifiers. When the
  ;; `define-with-contract` macro is used and one writes an
  ;; expression like (require ...), the identifier `require`
  ;; is used, instead of it being pure syntax. The advantage
  ;; is, that the identifier can be renamed, when imported
  ;; in another module. This enables users to change how
  ;; macro call looks. They might want to change `ensure` to
  ;; `make-sure` or `post-condition`, or any other
  ;; renaming. For example like the following import:

  ;; (import
  ;;  (rename (contract)
  ;;          (require req)
  ;;          (ensure ens)))

  ;; Note, that even though `syntax-rules` specifies
  ;; "literals", specifying <?> still works and still allows
  ;; for renaming in another module. Very useful!
  (define require 'require)
  (define ensure 'ensure)
  ;; Using vectors here, because eq? does not return #t for
  ;; (eq? v1 v2). This means only comparing to the same
  ;; object will return #t.
  (define unknown-origin (vector "unknown origin"))


  (define-syntax define-with-contract
    (syntax-rules (require ensure)
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (lambda (args* ...)
            lambda-body-expr* ...))
       (define function-name
         (lambda-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...))]

      [(_ (function-name args* ...)
          (require reqs* ...)
          (ensure ensu-expr* ...)
          lambda-body-expr* ...)
       (define function-name
         (lambda-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...))]

      ;; Catch all other cases, including the ones with rest
      ;; arguments.
      [(_ args* ...)
       (define*-with-contract args* ...)]))


  (define-syntax define*-with-contract
    (syntax-rules (require ensure)
      ;; definitions without rest args
      ;; short definition
      [(_ (function-name args* ...)
          (require reqs* ...)
          (ensure ensu-expr* ...)
          lambda-body-expr* ...)
       (define function-name
         (lambda*-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...))]
      ;; long definition
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...)
       (define function-name
         (lambda*-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...))]

      ;; definitions with rest args
      ;; shortened definition
      [(_ (function-name args* ... . rest-args)
          (require reqs* ...)
          (ensure ensu-expr* ...)
          lambda-body-expr* ...)
       (define function-name
         (lambda*-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ... . rest-args)
          lambda-body-expr* ...))]
      ;; long definition
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ... . rest-args)
          lambda-body-expr* ...)
       (define function-name
         (lambda*-with-contract
          function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ... . rest-args)
          lambda-body-expr* ...))]))

  ;; `lambda-with-contract` is implemented in terms of
  ;; `lambda*-with-contract`.
  (define-syntax lambda-with-contract
    (syntax-rules (require ensure)
      ;; CASE 1: A case for when `lambda-with-contract` is
      ;; called without a function name. This should be the
      ;; case, when `lambda-with-contract` is used directly,
      ;; without the indirection through a
      ;; `define-with-contract` call.
      [(_ (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...)
       ;; Redirect to version with origin, but giving the origin
       ;; `unknown-origin`, since it is unknown.
       (lambda-with-contract unknown-origin
                             (require reqs* ...)
                             (ensure ensu-expr* ...)
                             (args* ...)
                             lambda-body-expr* ...)]
      ;; CASE 2: A case for a call with an additional
      ;; function name. In case `lambda-with-contract` is
      ;; called from define-with-contract, it should be
      ;; called with a function name.
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...)
       ;; Redirect to most general case.
       (lambda*-with-contract function-name
                              (require reqs* ...)
                              (ensure ensu-expr* ...)
                              (args* ...)
                              lambda-body-expr* ...)]

      ;; Catch all other cases, including the ones with rest
      ;; arguments.
      [(_ args* ...)
       (lambda*-with-contract args* ...)]))


  ;; Example usage:

  ;; ((lambda-with-contract
  ;;   (require (> a 0))
  ;;   (ensure (> ((λ (res) (+ res 1)) <>) 0))
  ;;   (a b)
  ;;   (+ a b)) 1 -1)


  ;; `lambda*-with-contract` is the macro, which is the
  ;; entrypoint to calling CK macros. It is also used for
  ;; implementing `lambda-with-contract`,
  ;; `define-with-contract` and `define*-with-contract`.
  (define-syntax lambda*-with-contract
    (syntax-rules (require ensure unknown-origin)
      ;; CASE 1: A case for when `lambda-with-contract` is
      ;; called without a function name. This should be the
      ;; case, when `lambda-with-contract` is used directly,
      ;; without the indirection through a
      ;; `define-with-contract` call. In this case an
      ;; artificial function name is used, which is defined
      ;; above.
      [(_ (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...)

       ;; If no function-name has been given, call with
       ;; unknown-origin as function name.
       (lambda*-with-contract unknown-origin
                              (require reqs* ...)
                              (ensure ensu-expr* ...)
                              (args* ...)
                              lambda-body-expr* ...)]

      ;; CASE 2: A case for a call with an additional
      ;; function name. `lambda-with-contract` should be
      ;; called with function name from a
      ;; define-with-contract call, but not with function
      ;; name, when used directly.
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ...)
          lambda-body-expr* ...)

       (lambda* (args* ...)
         ;; Check, whether the function name is known.
         (let* ([pre-condition-check-result
                 ;; Check the requirements (pre-conditions).
                 (if (eq? function-name unknown-origin)
                     (ck () (c-and-raise
                             (quote "unknown origin")
                             (c-map '(c-replace-placeholder 'result)
                                    '(list reqs* ...))))
                     (ck () (c-and-raise
                             (quote function-name)
                             (c-map '(c-replace-placeholder 'result)
                                    '(list reqs* ...)))))])

           ;; Temporarily store result of the function.
           (let ([result
                  ;; Run the actual code of the contracted
                  ;; procedure.
                  (begin
                    lambda-body-expr* ...)])

             (let ([post-condition-check-result
                    ;; Check ensured conditions (post-conditions).
                    (if (eq? function-name unknown-origin)
                        (ck () (c-and-raise
                            (quote "unknown origin")
                            (c-map '(c-replace-placeholder 'result)
                                   '(list ensu-expr* ...))))
                        (ck () (c-and-raise
                                (quote function-name)
                                (c-map '(c-replace-placeholder 'result)
                                       '(list ensu-expr* ...)))))])
               post-condition-check-result)

             ;; Return result, if post-conditions are true.
             result)))]

      ;; Cases for rest arguments.
      [(_ (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ... . rest-args)
          lambda-body-expr* ...)
       (lambda*-with-contract unknown-origin
                              (require reqs* ...)
                              (ensure ensu-expr* ...)
                              (args* ... . rest-args)
                              lambda-body-expr* ...)]
      [(_ function-name
          (require reqs* ...)
          (ensure ensu-expr* ...)
          (args* ... . rest-args)
          lambda-body-expr* ...)

       (lambda* (args* ... . rest-args)
         (let* ([pre-condition-check-result
                 (if (eq? function-name unknown-origin)
                     (ck () (c-and-raise
                             (quote "unknown origin")
                             (c-map '(c-replace-placeholder 'result)
                                    '(list reqs* ...))))
                     (ck () (c-and-raise
                             (quote function-name)
                             (c-map '(c-replace-placeholder 'result)
                                    '(list reqs* ...)))))])
           (let ([result (begin lambda-body-expr* ...)])
             (let ([post-condition-check-result
                    (if (eq? function-name unknown-origin)
                        (ck () (c-and-raise
                            (quote "unknown origin")
                            (c-map '(c-replace-placeholder 'result)
                                   '(list ensu-expr* ...))))
                        (ck () (c-and-raise
                                (quote function-name)
                                (c-map '(c-replace-placeholder 'result)
                                       '(list ensu-expr* ...)))))])
               post-condition-check-result)
             result)))]))

  ;; Make λ and λ* aliases for lambda-with-contract and
  ;; lambda*-with-contract.
  (define-syntax λ*-with-contract
    ;; TODO: Are the literaly really needed here?
    (syntax-rules (require ensure unknown-origin)
      [(_ args* ...)
       (lambda*-with-contract args* ...)]))

  (define-syntax λ-with-contract
    ;; TODO: Are the literaly really needed here?
    (syntax-rules (require ensure unknown-origin)
      [(_ args* ...)
       (lambda-with-contract args* ...)])))
